(set-logic QF_BV)
(declare-fun x0 () Bool)
(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun x3 () Bool)
(declare-fun x4 () Bool)
(declare-fun x5 () Bool)
(declare-fun x6 () Bool)
(declare-fun x7 () Bool)
(declare-fun x8 () Bool)
(declare-fun x9 () (_ BitVec 32))
(declare-fun x10 () (_ BitVec 32))
(assert (let ((?v_58 (bvadd (bvsub x2 x1) (_ bv65536 32)))) (let ((?v_50 (bvadd (bvsub (_ bv0 32) ?v_58) x10))) (let ((?v_54 (bvadd (bvsub x2 ?v_50) (_ bv65536 32))) (?v_9 (bvadd (_ bv0 32) (_ bv513 32)))) (let ((?v_46 (bvadd (bvsub ?v_9 ?v_54) x10))) (and true (bvslt (_ bv0 32) x9) x3 (bvslt ?v_46 (_ bv254 32)) x7 true x4 true (bvslt ?v_50 (_ bv254 32)) (bvslt (_ bv0 32) ?v_50) true x8 true x0 true x6 true x5 true))))))
(check-sat)
(exit)
